Article Preview
Top1. Introduction
System of systems (SoS) (Maier, 1996) are an emerging class of complex, distributed and independent systems that are cooperating and interacting to accomplish specific goals, known as SoS missions, which neither of them can achieve nor obtain on its own. Various challenges have to be considered when modelling and specifying a SoS, as for instance: 1) Missions: they represent the main goal of a SoS and its desired behaviour that it needs to attend. Several constituent systems may combine their roles to achieve a certain mission. 2) Interactions: A mission of a SoS can only be achieved by a cooperation between its constituent systems. 3) Hierarchy: A SoS is constituted with a set of sub-systems. Each one may also be a SoS. These constituents are, autonomous and operating independently. Besides, they may operate to achieve the SoS mission. 4) Evolution: The constituent systems are constantly changing their interactions and role combinations, yielding to dynamic behaviours of a SoS. 5) Dynamic Controls: A SoS dynamic evolution should be controlled, to prohibit undesired behaviours that may occur in the SoS and in its constituents.
In order to overcome these challenges and to capture the dynamic nature of a SoS, we have defined in a previous work ArchSoS (Seghiri et al., 2018), a formal Architectural Description Language (ADL). Its main purpose is to model hierarchical structures of these systems and their reconfigurations, as well as the ability to manage potential cooperation between their constituent systems.
In this paper, we extend ArchSoS by a syntax-driven description, that has the ability to model SoS constituents, and the events affecting them, as well as their behavioural constraints.
Particularly, the main objective of this paper is twofold. On one hand, a formal and graphical syntax, inspired by Bigraphic Reactive Systems (BRS) principle (Milner, 2001) is given to ArchSoS. This will offer a syntax-driven SoS description, dealing with the hierarchy concepts and interactions between systems. On the other hand, a guided rewriting-based operational semantic is associated to ArchSoS. Rewrite theories (Meseguer, 1996) seem to be appropriate for defining a SoS semantic. ArchSoS specifications are implemented using Maude language (Clavel et al., 2007) to execute and simulate them, while analyzing their pertinent properties.
A Bigraphic Reactive System (BRS) is a formalism for describing and modelling computational systems. It contains a Bigraph model, representing the structural aspect of a system, and a set of Reaction Rules to describe how bigraphical components may be reconfigured, defining the semantic of a system. A Bigraph is defined by a set of nodes and a set of links between those nodes, known as edges. The nodes have the ability to be nested inside one another. A Bigraph may also have algebraic notations, which are equivalent to graphical ones. A reaction rule has the form R → R’, where R is called the redex (Bigraph before the state transition), and R' is the reactum (Bigraph after the state transition). Thus, in a transition of a Bigraph using a specified rule, the redex is the part of the Bigraph that is matched, and will be replaced by the matching part of the reactum.
We have chosen BRS as a base for modeling SoS systems since it allows a formal and visual technique for designing SoS software architectures, it provides enough expressive ability to represent not only SoS components and elements, but also their dynamic specification through the use of reaction rules.
On the other hand, Maude which is an implementation language based on Rewriting logic, is chosen as a formal semantic framework for ArchSoS. It uses a mathematical notations represented by a rewriting theory = (Σ,E,R, where the signature (Σ,E) describes its static structure, while the rewriting rules R describe its behaviour and evolution, our choice of using rewrite theories is justified by their ability of reasoning on concurrent systems, representing their states and their different transitions. Maude emphasizes simplicity, expressiveness and performance (Clavel et al., 2007), and offers a particular syntax using a set of sorts and operations to define concurrent computations between systems, allowing the execution of its formal specifications and formal verification.